/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓α␈↓ ∧%Correctness of Programs that Modify List Structure

␈↓ α∧␈↓␈↓ αTConsider the LISP program ␈↓↓nconc␈↓ defined by

␈↓ α∧␈↓nconc[u,v] ← ␈↓αif␈↓ ␈↓αn␈↓ u ␈↓αthen␈↓ v ␈↓αelse␈↓ prog[[w]

␈↓ α∧␈↓␈↓ αTw ← u l: ␈↓αif␈↓ ␈↓αn␈↓ ␈↓αd␈↓ w ␈↓αthen␈↓ qbegin jnk ← rplacd[w,v]; return u qend;

␈↓ α∧␈↓␈↓ αTw ← ␈↓αd␈↓ w

␈↓ α∧␈↓␈↓ αTqgo l]

␈↓ α∧␈↓␈↓ αT␈↓↓nconc␈↓␈αis␈αa␈αdestructive␈α
version␈αof␈α␈↓↓append␈↓␈αin␈α
that␈αa␈αvariable␈αwhose␈α
value␈αis␈α␈↓↓u␈↓␈αis␈α
changed␈αto
␈↓ α∧␈↓have␈αvalue␈α␈↓↓u*v.␈αOther␈↓␈αvariables␈αare␈αunchanged␈αif␈αthey␈αdon't␈αmerge␈αwith␈αthe␈αtop␈αlevel␈αof␈α␈↓↓u.␈↓␈αHow
␈↓ α∧␈↓shall we state this formally and prove it?

␈↓ α∧␈↓␈↓ αTWe␈α∂begin␈α⊂by␈α∂distinguishing␈α⊂between␈α∂S-expressions␈α⊂and␈α∂pointers␈α⊂and␈α∂by␈α⊂introducing␈α∂the
␈↓ α∧␈↓memory␈α∞state␈α∂␈↓↓mem␈↓␈α∞and␈α∞the␈α∂function␈α∞␈↓↓val(uu,m).␈↓␈α∞We␈α∂shall␈α∞use␈α∞single␈α∂letters␈α∞for␈α∂variables␈α∞whose
␈↓ α∧␈↓values␈α
are␈α
S-expressions␈α∞and␈α
doubled␈α
letters␈α∞for␈α
variables␈α
whose␈α∞values␈α
are␈α
pointers.␈α∞ A␈α
typical
␈↓ α∧␈↓relation might be

␈↓ α∧␈↓␈↓ αT␈↓↓val(xx,mem) = x␈↓

␈↓ α∧␈↓␈↓ αTmeaning␈αthat␈α
the␈αpointer␈α␈↓↓xx␈↓␈α
points␈αto␈αa␈α
list␈αstructure␈αrepresenting␈α
the␈αS-expression␈αwhich␈α
is
␈↓ α∧␈↓the value of the S-expression variable ␈↓↓x.␈↓

␈↓ α∧␈↓␈↓ αTWe␈α⊃now␈α⊃introduce␈α⊂␈↓↓nconc(xx, vv, mem)␈↓␈α⊃as␈α⊃a␈α⊂two␈α⊃output␈α⊃function␈α⊂whose␈α⊃value␈α⊃is␈α⊃a␈α⊂new
␈↓ α∧␈↓pointer and a new memory state.  We shall want to prove

␈↓ α∧␈↓␈↓ αT␈↓↓∀uu mem. val(nconc(uu, vv, mem) = val(uu, mem) * val(vv, mem)␈↓

␈↓ α∧␈↓␈↓ αTas␈α∞the␈α∂relation␈α∞between␈α∂␈↓↓nconc␈↓␈α∞and␈α∂␈↓↓append.␈↓␈α∞However,␈α∂this␈α∞isn't␈α∂all␈α∞we␈α∂will␈α∞need␈α∂to␈α∞prove
␈↓ α∧␈↓about ␈↓↓nconc.␈↓

␈↓ α∧␈↓␈↓ αTThe program can now be written cleanly as

␈↓ α∧␈↓␈↓ αT␈↓↓nconc[uu, vv, mem] ← ␈↓αif␈↓↓ null[uu, mem] ␈↓αthen␈↓↓ vv, mem ␈↓αelse␈↓↓ prog[[ww, jjnk]

␈↓ α∧␈↓↓␈↓ αTww␈α∀←␈α∀uu;␈α∀l:␈α∀␈↓αif␈↓↓␈α∀null␈α∀cdr[ww,␈α∃mem]␈α∀␈↓αthen␈↓↓␈α∀qbegin␈α∀jjnk,␈α∀mem␈α∀←␈α∀rplacd[ww,␈α∃vv,␈α∀mem]
␈↓ α∧␈↓↓return2[uu, mem] qend;

␈↓ α∧␈↓↓␈↓ αTww ← cdr[ww, mem];

␈↓ α∧␈↓↓␈↓ αTqgo l]␈↓.

␈↓ α∧␈↓↓␈↓ αTPerhaps␈α∩we␈α∩should␈α∩now␈α∩try␈α∩to␈α∩elephantize␈α∩the␈α∩program,␈α∩but␈α∩it␈α∩still␈α∩isn't␈α∩clear␈α∪how␈α∩to
␈↓ α∧␈↓↓elephantize function calls.